Inference at * 1 2 1 
Iof proof for Lemma mul cancel in eq:



1. a : 
2. b : 
3. n : 
4. m:. ((m * a) = (m * b))  (a = b)
5. (n * a) = (n * b)
6. n > 0
  a = b 

latex

 by ((Using [`m',n] (BackThruHyp 4)) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions

t  T, , i > j, P  Q, x:A. B(x),